\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Out}$, ${\it Sys}$:AbsInterface(Top), ${\it Ack}$:AbsInterface($\mathbb{N}$), $g$:sys{-}antecedent(${\it es}$;${\it Ack}$),\+
\\[0ex]${\it chain}$:(\{$e$:E$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Ack}$))\} $\rightarrow$(Id List)).
\-\\[0ex](E(${\it Out}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]$\Rightarrow$ chain{-}config(${\it es}$;p{-}conditional(${\it Ack}$; ${\it Sys}$);${\it chain}$)
\\[0ex]$\Rightarrow$ ($\forall$$e$:E(${\it Sys}$). ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)) $\Rightarrow$ (loc($e$) = last(${\it chain}$($e$)) $\in$ Id))
\\[0ex]$\Rightarrow$ \=($\forall$$e$:E(${\it Ack}$).\+
\\[0ex]($\neg$(loc($g$($e$)) = loc($e$) $\in$ Id))
\\[0ex]$\Rightarrow$ \=(adjacent(Id;${\it chain}$($e$);loc($e$);loc($g$($e$)))\+
\\[0ex]\& adjacent(Id;${\it chain}$($g$($e$));loc($e$);loc($g$($e$)))))
\-\-\\[0ex]$\Rightarrow$ ($\forall$$e$:E(${\it Ack}$). (loc($g$($e$)) = loc($e$) $\in$ Id) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]$\Rightarrow$ chain{-}consistent($g$;$\lambda$$e$.rev(${\it chain}$($e$)))
\end{tabbing}